T:Type, R:(TT), x, y:T. (x (R^*) y)  (L:T List. rel-path-between(T;R;x;y;L)) 

latex

Definitions	Type, x:A  B(x), x:A. B(x), x:AB(x), , type List, a < b, f(a), x f y, s = t, P & Q, x:A. B(x), hd(l), rel-path(R;L), rel-path-between(T;R;x;y;L), t  T, , <a, b>, , {x:A| B(x)} , #$n, n+m, ||as||, , P  Q, P  Q, (x  l), P  Q, x.A(x), x. t(x), rel_exp(T;R;n), R^*, |g|, S  T, A, b, Void, False, A  B, i  j , last(L), A c B, n * m, -n, n - m
Lemmas	member wf, le wf, rel-path wf, hd wf, last wf, assert wf, length wf1, all functionality wrt iff, iff functionality wrt iff, rel exp wf, exists functionality wrt iff, rel exp-iff-path, iff wf, rev implies wf, nat wf, rel-path-between wf